Inference at * 
Iof proof for Lemma p-co-filter wf:


  T:Type, P:(T), f:(x:T. Dec(P(x))). p-co-filter(f)  T(T + Top) 

latex

 by ((Unfolds ``all decidable p-co-filter`` 0) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions	Dec(P), p-co-filter(f), x.A(x), case b of inl(x) => s(x) | inr(y) => t(y), P  Q, left + right, , Type, A, f(a), inr x , x(s), x:A. B(x), x:AB(x), inl x , Top, x:A.B(x), t  T, Void
Lemmas	not wf, top wf